Nuprl Lemma : not-isl-priority-select
0,22
postcript
pdf
T
:Type,
as
:
T
List,
f
,
g
:(
T
).
isl(priority-select(
f
;
g
;
as
))
(
a
as
.
f
(
a
) &
g
(
a
))
latex
Definitions
Unit
,
t
T
,
,
x
:
A
.
B
(
x
)
,
priority-select(
f
;
g
;
as
)
,
P
Q
,
isl(
x
)
,
b
,
A
,
,
Prop
,
P
&
Q
,
x
.
t
(
x
)
,
x
L
.
P
(
x
)
,
P
Q
,
P
Q
,
True
,
False
Lemmas
false
wf
,
iff
functionality
wrt
iff
,
priority-select-inr
,
l
all
wf
,
it
wf
,
not
wf
,
assert
wf
,
isl
wf
,
priority-select
wf
,
bool
wf
,
unit
wf
origin
T:Type, as:T List, f, g:(T
). 
isl(priority-select(f;g;as)) 
(a
as. f(a) & g(a)) T:Type, as:T List, f, g:(T). isl(priority-select(f;g;as)) (aas. f(a) & g(a)) Tx:A. B(x)
Q
bA
x. t(x)xL. P(x) Q Q